data specification using nat natinf = ā . ā(. .n : nat) | ā ; variables nā : natinf; end data specification